| 1: | minus(0,y) | → 0 | |
| 2: | minus(s(x),0) | → s(x) | |
| 3: | minus(s(x),s(y)) | → minus(x,y) | |
| 4: | le(0,y) | → true | |
| 5: | le(s(x),0) | → false | |
| 6: | le(s(x),s(y)) | → le(x,y) | |
| 7: | if(true,x,y) | → x | |
| 8: | if(false,x,y) | → y | |
| 9: | perfectp(0) | → false | |
| 10: | perfectp(s(x)) | → f(x,s(0),s(x),s(x)) | |
| 11: | f(0,y,0,u) | → true | |
| 12: | f(0,y,s(z),u) | → false | |
| 13: | f(s(x),0,z,u) | → f(x,u,minus(z,s(x)),u) | |
| 14: | f(s(x),s(y),z,u) | → if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) | |
| 15: | MINUS(s(x),s(y)) | → MINUS(x,y) | |
| 16: | LE(s(x),s(y)) | → LE(x,y) | |
| 17: | PERFECTP(s(x)) | → F(x,s(0),s(x),s(x)) | |
| 18: | F(s(x),0,z,u) | → F(x,u,minus(z,s(x)),u) | |
| 19: | F(s(x),0,z,u) | → MINUS(z,s(x)) | |
| 20: | F(s(x),s(y),z,u) | → IF(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) | |
| 21: | F(s(x),s(y),z,u) | → LE(x,y) | |
| 22: | F(s(x),s(y),z,u) | → F(s(x),minus(y,x),z,u) | |
| 23: | F(s(x),s(y),z,u) | → MINUS(y,x) | |
| 24: | F(s(x),s(y),z,u) | → F(x,u,z,u) | |